Termination Proof Script

• Consider the SCC {10,27-30}. The usable rules are {1,6-8}. By taking the AF π with π(active) = π(ACTIVE) = π(f) = π(F) = π(mark) = 1 together with the lexicographic path order with empty precedence, the rules in {1,6-8,10,27,28,30} are weakly decreasing and rule 29 is strictly decreasing. There is one new SCC.
  • Consider the SCC {10,27,28,30}. By taking the AF π with π(ACTIVE) = π(f) = π(F) = π(mark) = π(no) = 1 together with the lexicographic path order with empty precedence, the rules in {6-8,10,30} are weakly decreasing and the rules in {1,27,28} are strictly decreasing. There is one new SCC.
    • Consider the SCC {30}. There are no usable rules. By taking the AF π with π(F) = 1 together with the lexicographic path order with empty precedence, rule 30 is strictly decreasing.


• Consider the SCC {12}. The usable rules are {1,3,5-8}. By taking the AF π with π(active) = π(CHK) = π(no) = 1, π(mat) = 2 and π(mark) = [ ] together with the lexicographic path order with precedence f ≻ mark, the rules in {3,5-7} are weakly decreasing and the rules in {1,8,12} are strictly decreasing.


• Consider the SCC {31}. The usable rules are {1-8}. The constraints could not be solved.